Note: The numbers attached to each option represents the corresponding options under batch mode verification and command line console.

Deadlock-Freeness and Nonterminating:

• Admissible behaviors: All (0)
• Verification engines:
  • First witness trace using Depth First Search (0)
  • Shortest witness trace using Breadth First Search (1)
  • Symbolic Model Checking using BDD with Forward Search Strategy (2)
  • Symbolic Model Checking using BDD with Backward Search Strategy (3)
  • Symbolic Model Checking using BDD with Forward-Backward Search Strategy (4)

Divergence-Freeness andDeterministic:

• Admissible behaviors: All (0)
• Verification engines:
  • First witness trace using Depth First Search (0)
  • Shortest witness trace using Breadth First Search (1)

Reachability:

• Admissible behaviors: All (0)
• Verification engines:
  • First witness trace using Depth First Search (0)
  • Shortest witness trace using Breadth First Search (1)
  • Symbolic Model Checking using BDD with Forward Search Strategy (2)
  • Symbolic Model Checking using BDD with Backward Search Strategy (3)
  • Symbolic Model Checking using BDD with Forward-Backward Search Strategy (4)

Refinement:

• Admissible behaviors: All (0)
• Verification engines:
  • On-the-fly trace refinement checking using Depth First Search (0)
  • On-the-fly trace refinement checking using Breadth First Search (1)

Failure-Refinement:

• Admissible behaviors: All (0)
• Verification engines:
  • On-the-fly failure refinement checking using Depth First Search (0)
  • On-the-fly failure refinement checking using Breadth First Search (1)

Failure/Divergence Refinement:

• Admissible behaviors: All (0)
• Verification engines:
  • On-the-fly failures/divergence refinement checking using Depth First Search (0)
  • On-the-fly failures/divergence refinement checking using Breadth First Search (1)

Safety-LTL Properties:

• Admissible behaviors: All (0)
• Verification engines:
  • Strongly connected components based search (0)
  • Symbolic model checking using BDD (1)

Liveness Properties: (for the meaning of admissible behaviors with fairness assumption, please refer to Section 4.1)

• Admissible behaviors:
  • All (0)
  • Event-level weak fair only (1)
  • Event-level strong fair only (2)
  • Process-level weak fair only (3)
  • Process-level strong fair only (4)
  • Global fair only (5)
• Verification engines (same for each admissible behavior above):
  • Strongly connected components based search (0)
  • Symbolic model checking using BDD (1)